COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(declare (special refuted d c p n) (fixsw t))
C00007 ENDMK
C⊗;
(declare (special refuted d c p n) (fixsw t))

(defun implies (premise conclusion)
;      (format t "Trying to prove that ~S implies ~s ~%"
;	       premise conclusion)
       (add-conjunction premise (opposite conclusion) () () () ()))

(defun opposite (f)
       (prog (O)
	     (setq o (car f))
	     (return
	      (cond ((eq o 'AND)
		     `(or ,(opposite (cadr f)) . ,(opposite (cddr f))))
		    ((eq o 'or)
		     `(and  ,(opposite (cadr f)) . ,(opposite (cddr f))))
		    ((eq O '+)
		     `(- . ,(cdr f)))
 		    ((eq O '-)
		     `(+ . ,(cdr f)))))))

(defun add-conjunction (f g d c p n)
       (prog (refuted)
;	     (format t "Expanding conjunction ~S by Rule 1 ~%"
;		     `(and  ,f . ,g))
	     (setq refuted ())
	     (expand f)
	     (expand g)
	     (cond 
	      (refuted
;	       (format t "Contradiction spotted~%")
	       (return t))
	      ((not (atom d))
	       (return (split (cadr (car d))
			      (cddr (car d))
			      (cdr d))))
	      (t 
	       ;(format t "Cannot refute ~S ~S ~S ~S ~%" d c p n)
	       (return ())))))

(defun split (f1 g1 d)
       (prog (f g)
;	     (format t "Case analysis on ~S (Rule 2)~%"
;		     `(or ,f . ,g))
	     (setq f (opposite f1))
	     (setq g (opposite g1))
	     (return
	      (and (add-conjunction f  g1 d c p n)
		   (add-conjunction f  g  d c p n)
		   (add-conjunction f1 g  d c p n)))))

(defun expand (f)
       (prog (o)
	     (setq o (car f))
	     (cond ((eq o 'and)
		    (cond ((member f d)
			   (setq refuted t))
			  ((member f c)
			   ())
			  (t (setq c `(,f . ,c))
			     (expand (cadr f))
			     (expand (cddr f)))))
		   ((eq o 'or)
		    (setq d (extend (opposite f) d c)))
		   ((eq o '+)
		    (setq p (extend (cdr f) p n)))
		   ((eq o '-)
		    (setq n (extend (cdr f) n p))))
	     (return ())))

(defun extend (f a b)
       (cond ((member f b)
	      (setq refuted t) a)
	     ((member f a) a)
	     (t `(,f . ,a))))

(defmacro try (p c  m)
 `(do ((i ,(// m 10.) (1- i)))
      ((= i 0) t)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)
      (implies ,p ,c)))

(include "timer.lsp")
(timer timit
       (progn 
	(try '(- . a) '(+ . a) 1000.)
	(try  '(+ . b) '(or (- . b) . (- . b)) 1000.)
	(try '(+ . nothing) '(or (+ . to-be) . (- . to-be)) 1000.)
	(try '(or (- . a) . (- . a)) '(- . a) 1000.)
	(try '(- . b) '(or (+ . a) . (- . b)) 1000.)
	(try '(and (- . a) . (- . b))
	       '(and (- . b) . (- . a)) 1000.)
	(try '(- . b) '(or (- . a) . (and (+ . a) . (- . b))) 1000.)
	(try '(or (- . a) . (or (- . b) . (+ . c)))
	     '(or (- . b) . (or (- . a) . (+ . c))) 1000.)
	(try '(or ( - . a) . (+ . b))
	     '(or (and (+ . b) . (- . c))
				   . (or (- . a) . (+ . c))) 1000.)
	(try '(and (or (- . a) . ( + . c)).
		   (or (- . b) . (+ . c)))
	     '(or (and (- . a) . (- . b)) . (+ . c)) 1000.)))